Termination Proof Script

Consider the TRS R consisting of the rewrite rule


1:	app(app(app(uncurry,f),x),y)	→ app(app(f,x),y)

There are 2 dependency pairs:


2:	APP(app(app(uncurry,f),x),y)	→ APP(app(f,x),y)
3:	APP(app(app(uncurry,f),x),y)	→ APP(f,x)

Consider the SCC {2,3}. By taking the AF π with π(APP) = 1 together with the lexicographic path order with empty precedence, the rules in {1-3} are strictly decreasing. Hence the TRS is terminating.

Tyrolean Termination Tool (0.01 seconds) --- May 3, 2006